Publications of
Nassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai
Expérimentations en Coq pour un générateur de code qualifiable
In : Revue des Sciences et Technologies de l’Information, Technique et Science Informatiques, Hermès Science, Special issue Méthodes formelles à l’analyse et la compilation, Vol. 30, N. 4/2011, pp. 409-440, April 2011.
Benoit Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux
Essay on Semantics Definition in MDE. An Instrumented Approach for Model Verification.
In : Journal of Software (JSW), Academy Publisher, Finland, Vol. 4 N. 6, pp. 943-958, November 2009.
Abstract URL : http://www.academypublisher.com/ojs/index.php/jsw/article/view/0409943958
BibTeXBenoit Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux, François Vernadat
A Property-Driven Approach to Formal Verification of Process Models
In : Enterprise Information Systems, Taylor & Francis Online, Special issue LNBIP 12, ICEIS 2007, Revised Selected Papers, Vol. 12, pp. 286-300, 2009.
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
Abstract Interpretation-based Static Safety for Actors
In : Journal of Software (JSW), Academy Publisher, Finland, Vol. 2 N. 3, pp. 87-98, September 2007.
Philippe Mauran, Philippe Quéinnec, Xavier Thirioux
Teaching Transition Systems and Formal Specifications with TLA+ (regular paper)
In : International Workshop on the TLA+ Method and Tools, Paris, France, 27/08/12, Kent State UNiversity, (electronic medium), August 2012.
URL : http://queinnec.perso.enseeiht.fr/publis/TLA2012.pdf
BibTeXMounira Kezadri, Benoit Combemale, Marc Pantel, Xavier Thirioux
A proof assistant based formalization of MDE components (regular paper)
In : Formal Aspects of Component Software (FACS 2011), Oslo, Norway, 14/09/11-16/09/11, Vol. 7253, Springer, Lecture Notes in Computer Science, (electronic medium), September 2011.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux
Machine-Checked Sequencer for Critical Embedded Code Generator (regular paper)
In : Formalisation des Activités Concurrentes (FAC 2010), Toulouse, France, 31/03/10-01/04/10, ONERA, (electronic medium), April 2010.
Nassima Izerrouken, Olivier Ssi Yan Kai, Marc Pantel, Xavier Thirioux
Use of Formal Methods for Building Qualified Code Generator for Safer Automotive Systems (regular paper)
In : Critical Automotive applications: Robustness & Safety @ European Dependable Computing Conference (CARS@EDCC 2010), Valencia, 27/04/10-30/04/10, ACM : Association for Computing Machinery, pp. 53-56, April 2010.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux
Ordonnanceur vérifié pour un générateur de code automatique qualifiable (regular paper)
In : Formalisation des Activités Concurrentes (FAC 2009), Toulouse, France, 01/04/09, IRIT, (on line), April 2009.
URL : http://seminaire-verif.enseeiht.fr/FAC/2009/Papiers/32.pdf
BibTeXNassima Izerrouken, Marc Pantel, Xavier Thirioux, Olivier Ssi Yan Kai
Integrated Formal Approach for Qualified Critical Embedded Code Generator (short paper)
In : International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2009), Eindhoven – The Netherlands, 02/11/09-03/11/09, Springer-Verlag, pp. 199-201, 2009.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux
Machine Checked Sequencer for Critical Embedded Code Generator (regular paper)
In : International Conference on Formal Engineering Methods (ICFEM 2009), Rio de Janeiro, Brazil, 09/12/09-12/12/09, Springer-Verlag, pp. 521-540, December 2009.
Nassima Izerrouken, Marc Pantel, Xavier Thirioux, Martin Strecker
Certifying an Automated Code Generator Using Formal Tools: Preliminary experiments in the GeneAuto project (regular paper)
In : Formalisation des Activités Concurrentes (FAC 2008), Toulouse, France, 03/04/08-04/04/08, LAAS, (on line), April 2008.
URL : http://seminaire-verif.enseeiht.fr/FAC/2008/Papiers/53.pdf
BibTeXNassima Izerrouken, Xavier Thirioux, Marc Pantel, Martin Strecker
Certifying an Automated Code Generator Using Formal Tools : Preliminary Experiments in the GeneAuto Project
In : European Congress on Embedded Real-Time Software (ERTS 2008), Toulouse, 29/01/08-01/02/08, Société des Ingénieurs de l’Automobile, (electronic medium), 2008.
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
Spécification et Vérification par Interprétation Abstraite d’Aspects pour la Distribution
In : Formalisation des Activités Concurrentes (FAC 2007), Toulouse, France, 16/03/07-16/03/07, CNRS, (on line), March 2007.
Xavier Thirioux, Benoit Combemale, Xavier Crégut, Pierre-Loïc Garoche
A Framework to formalise the MDE Foundations
In : International Workshop on Towers of Models (TOWERS 2007), Zurich, 25/06/07, Richard Paige, Jean Bézivin (Eds.), Model Driven Engineering (MDE), pp. 14-30, June 2007.
Benoit Combemale, Pierre-Loïc Garoche, Xavier Crégut, Xavier Thirioux, François Vernadat
Towards a Formal Verification of Process Model’s Properties – SimplePDL and TOCL Case Study
In : International Conference on Enterprise Information Systems (ICEIS 2007), Funchal, Madeira – Portugal, 12/06/07-16/06/07, INSTICC Press, pp. 80-89, June 2007 (Best paper).
Benoit Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux
Expérimentation pour la définition d’une sémantique dans l’IDM
In : Sémantique des (meta)Modèles, Toulouse, France, 29/01/07, INPT : Institut National Polytechnique de Toulouse, pp. 146-161, March 2007.
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
Static Analysis of Actors: From Type Systems to Abstract Interpretation
In : International Workshop on Emerging Applications of Abstract Interpretation (EAAI 2006), Vienna, Austria, 25/03/06-02/04/06, Francesco Ranzato (Eds.).
Pierre-Loïc Garoche, Marc Pantel, Xavier Thirioux
Static Safety for an Actor Dedicated Process Calculus by Abstract Interpretation
In : IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2006), Bologna, Italy, 14/06/06-16/06/06, Vol. 4037, Roberto Gorrieri, Heike Wehrheim (Eds.), Springer, LNCS , pp. 78-92, June 2006.
Matthias Colin, Marc Pantel, Xavier Thirioux
Analyse statique de la communication dans un langage d’Acteurs
In : Formalisation des Activités Concurrentes, Toulouse, 12/03/03-13/03/03, Mamoun Filali, Pierre Michel, François Vernadat (Eds.), Actes électroniques FERIA-SVF, pp. 1-18, March 2003.
Matthias Colin, Xavier Thirioux, Marc Pantel
Temporal logic based static analysis for non uniform behaviours
In : Formal Methods for Open Object-based Distributed Systems, Paris, 19/11/03-21/11/03, Springer Verlag – LNCS, pp. 94-108, November 2003.
Simple and Efficient Translation from LTL Formulas to Buchi Automata
In : Workshop on Formal Methods for Industrial Critical Systems, Malaga, 12/07/02-13/07/02, Elsevier, July 2002.
Abstract URL : http://www1.elsevier.com/gej-ng/31/29/23/120/53/show/Products/notes/index.htt
BibTeXMamoun Filali, Philippe Mauran, Gérard Padiou, Philippe Quéinnec, Xavier Thirioux
Refinement based validation of a distributed termination detection algorithm
In : International Workshop FMPPTA’2000, Cancun, 05/05/00, ., May 2000.
Xavier Thirioux, Gérard Padiou
Etude comparative de deux techniques de preuve de programmes Unity
In : AFADL : Approches formelles dans l’assistance au développement de logiciels, Toulouse, ONERA-CERT, pp. 177-188, May 1997.
Xavier Thirioux, Gérard Padiou
Assistance à la preuve de programmes Unity à l’aide du démonstrateur Coq
In : Journées du PRC de Programmation, Orléans, .
Vérification de propriétés temporelles de systèmes réactifs répartis
Master’s Thesis, Institut National Polytechnique de Toulouse, November 1999.